forall a: forall b:
O:a,b^ = O:b,a